$\forall$$T$, ${\it T'}$:Type\{i\}, $L$:($T$ List), $f$:(\{$t$:$T$$\mid$ ($t$ $\in$ $L$)\} $\rightarrow$${\it T'}$), $P$:(${\it T'}$$\rightarrow$${\it T'}$$\rightarrow\mathbb{P}$\{i'\}).
\\[0ex]($\forall$$x$,$y$$\in$map($f$;$L$).  $P$($x$,$y$)) $\Leftarrow\!\Rightarrow$ ($\forall$$x$,$y$$\in$$L$.  $P$($f$($x$),$f$($y$)))